Notes (Week 3 Monday)
These are the notes I wrote during the lecture.
Choose your own adventure!
(1) Finish up last week's slides (the logic bit)
(2) Move on to this week's slides (induction and recursion)
Option 2 wins in a landslide!
Q: In W1 we talked about using logic to reason about programs.
Is the relevance of (mathematical) recursion and induction
to reason about recursive programs?
A: Yes, but not only recursive programs.
More generally: it's relevant for reasoning about
*terminating* programs
quicksort(xs):
partition xs into one big pile: ys
and one element x (the pivot)
partition ys into two piles:
- zs (the elements smaller than x)
- ws (the elements not smaller than x)
quicksort(zs)
quicksort(ws)
^ merge them together in order
Q: Is it always possible to translate a recursive program into an
iterative program?
A: Yes it is. This is a famous folk theorem!
Q: What above vice versa?
A: Yes this is also possible.
For more on the theory of why this works: see Church-Turing thesis
which shows that turing machines (basically iterative programs)
and lambda calculus (basically recursive programs)
are equally expressive
== The difference between recursion in the mathematical sense,
and recursion in the programming sense ==
The difference between
mathematical functions (relations, input-output pairs)
programming functions (subroutines, a bunch of instructions
that happen when you call the function)
In programming,
you need base cases to make sure the function terminates
(doesn't run forever)
or (depending on the implementation) to prevent it from
blowing up the stack, integer overflow, ...
What about maths?
A: In the case of factorial, the definition is incomplete.
If all you know about a function is
(R) (n+1)! = (n+1)*(n!)
What exactly is the value of 1! ?
1! = (R)
1*0! = 0!
But we don't know what 0! is
Issue: there's no longer a unique function satisfying our equation.
Therefore: it's not a definition.
Q: What is the definition of a definition?
A: A property φ such that there is a unique x satisfying φ(x)
By leaving out the base case we lose the uniqueness property.
Suppose we "define" this "function":
f(x) = 1 + f(x) (R)
In programming:
this function will simply never terminate
In maths:
suppose a function satisfying (R) above exists
f(x) = 1 + f(x) by definition
^ cancel f(x) on both sides
0 = 1
thus: by allowing this kind of circular definition
we make false provable (we make our logic inconstitent)
f(x) = 1 + 2*f(x)
^ happens to have a unique solution in maths but not a useful program
To show that 2 is a natural number.
Note that 2 = 0+1+1
(1) O ∈ ℕ by (B)
(2) 0+1 ∈ ℕ by (R)
(3) 0+1+1 ∈ ℕ by (R)
We "defined" the natural numbers by
stating two properties of sets X:
0 ∈ X (1)
If n ∈ X then n+1 ∈ X (2)
But: the sets satisfying these properties
are not unique.
If we choose X := ℝ
properties (1) and (2) above are still true
If we choose X := ℕ
properties (1) and (2) above are also true
If we choose X := ℤ
properties (1) and (2) above are also true
The thing to notice is:
ℕ is a subset of every set that satisfies (1) and (2)
When we make an inductive definition of a set,
we implicitly mean the *least* (wrt subset inclusion)
set satisfying the property
The unique set Y satisfying (1) and (2) s.t.
Y ⊆ X for every X satisfying (1) and (2)
This set always exists because we can define Y as
the intersection of all such X
...but it might be empty.
Q: What if we take the singleton set satisfying 0 and
defining 0+1=0?
A: Yeah that works, but I'm assuming the "normal" def of +
Suppose I define 𝓝 to be the *least* set satisfying:
If n ∈ 𝓝 then n+1 ∈ 𝓝
The smallest set satisfying *only* this equation
turns out to be ∅.
With recursive functions:
you can make the definition incomplete by leaving out base cases
With recursive *sets*:
you just end up defining the empty set
struct node{
int data;
struct node *next;
}
^ this *looks* like a recursive data structure,
but in an important way it isn't.
This is related to the issue of termination:
recursively defined data structures contain
the things you can reach by starting from the base case
and building up using *finitely many* applications of
the recursive cases.
The C type node above allows for cyclic pointer structures.
node x;
x.data = 7;
x.next = &x;
// a linked list with just 7 over and over forever
This can be useful in programming, but it's not recursive
in the mathematical sense.
Instead of defining x in terms of *smaller* nodes,
we've defined it in terms of itself (circularly)
For now, we're interested in:
(1) only describing the linked lists that are actually recursive
(with no cycles)
(2) abstracting away from their concrete memory representation
In the notation of slide 27
the list usually written [2,3]
is here written (2,(3,⊥)) (assuming ⊥ represents empty list)
You can think of the natural numbers as
the linked list over a Data type with exactly one element.
(the unit type)
Q: Could you define arrays as a function from indexes to your data type?
A: Yes! This is often done in program verification.
This representation actually applies equally to linked lists.
By defining the propositional formulas inductively,
certain things are ruled out by construction that might otherwise not be.
E.g. we can't write infinite conjunctions
x_0 ∧ x_1 ∧ x_2 ∧ ...
^ this is not a formula, because there's no (finite) way to build it
from our formation rules.
Q: Is there any difference between inductive and recursive definitions?
A: Nope! They're synonyms.
I tend to use "recursive" when I talk about functions,
and "inductive" when I talk about sets.
Let's write a program to evaluate a propositional formula.
Remember: propositional formulas aren't necessarily
true or false on their own, to give them a truth value
you need to decide what the variables denote.
x ∧ ⊤ "x and True"
^ the truth value of this formula depends on the truth value of x.
σ denotes mappings from variable names to truth values.
We can define the truth value of a propositional formula
as a recursive function.
evaluate(σ,⊤) = ⊤
evaluate(σ,⊥) = ⊥
evaluate(σ,x) = σ(x)
evaluate(σ,¬φ) =
if evaluate(σ,φ) then
⊥
else ⊤
...
^ What we've done now is a
definition by structural
recursion over the definition
of wffs.
Every clause of the function
corresponds to a clause in the
definition of wffs
Every recursive call of the function
corresponds to a premise of one
of the (R) cases of the def.
Advantages of doing structural
recursion like this are:
- The program/function always terminates!
- It's easy to prove properties about
it by induction.
Theorem triang_closed_form:
∀n∈ℕ. sum(n) = sum2(n)
Proof
By basic induction on n.
(B): prove sum(0) = sum2(0)
sum(0) = 0 = 0*(0+1)/2 = sum2(0)
(I): assume sum(n) = sum2(n) (IH)
prove sum(n+1) = sum2(n+1)
sum(n+1) = (by def)
n+1 + sum(n) = (by IH)
n+1 + sum2(n) = (by def)
n+1 + (n*(n+1))/2 = (algebra)
...
(n+1)*(n+2)/2 = (by def)
sum2(n+1)
QED
Notice the close correspondence between the *definition* of ℕ
and the proof by induction principle
Definition of ℕ Induction principle of ℕ
(B) 0 ∈ ℕ (B) P(0)
(R) ∀n. n ∈ ℕ ⇒ n+1 ∈ ℕ (I) ∀n. P(n) ⇒ P(n+1)
these look exactly the same, except when we say "∈ ℕ" on the left,
we say "P" on the right.
Remember when we said that ℕ is the *least* set satisfying (B) and (R).
What you're really doing when you're doing a proof of P by induction,
is: showing that P is also a set that satisfies (B) and (R).
Because ℕ is the least such set, you're therefore proving
ℕ ⊆ P
Or equivalently:
∀n ∈ ℕ. P(n)
The natural numbers aren't the only thing with an induction principle!
In fact: every recursively defined set comes with an induction principle.
(structural induction)